1. $A$ : Type
\\[0ex]2. $L$ : $A$ List
\\[0ex]3. $n$ : $\mathbb{N}$
\\[0ex]4. $n$ $\leq$ $\parallel$$L$$\parallel$
\\[0ex]$\vdash$  $\parallel$nth\_tl($\parallel$$L$$\parallel$ {-} $n$;$L$)$\parallel$ = $n$